Issue3323r.agda:10,11-12
Unexpected modality/relevance annotation in .b
when checking the definition of R
